[Merged by Bors] - feat(Data/Finsupp): support of mapDomain is image of support if nonneg - #43610

PR summary fbf13c9d57

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit fbf13c9).

• +3 new declarations
• −0 removed declarations

+Finsupp.mapDomain_apply_of_injective
+Finsupp.prod_comapDomain
+Finsupp.support_mapDomain_of_nonneg

No changes to strong technical debt.
No changes to weak technical debt.

Current commit fbf13c9d57
Reference commit d1298f10ae

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

nit: use the "moves" section of the PR template

bors d+

✌️ YaelDillies can now approve this pull request until 2026-09-23 09:49 UTC (in 2 weeks). To approve and merge, reply with bors r+. More detailed instructions are available here.

⚠️ This delegation only covers changes within Archive/**, Counterexamples/**, docs/**, DownstreamTest/**, Mathlib/**, MathlibTest/**, Wanted/**, widget/**, Archive.lean, Counterexamples.lean, docs.lean, Mathlib.lean, Wanted.lean; an author commit touching anything else will revoke it. Bors also revokes it if a later push changes too many files for it to check the full list — even if it stays within scope.

bors merge

Your PR description says "since the latter is mathematically equivalent but stronger according to TC search." but this seems to be a reason not to do the change! In particular,

variable {M : Type*} [CommMonoid M] [Preorder M] [MulLeftMono M] in
#synth IsOrderedMonoid M

is false.

Build failed:

• ci (staging) / Post-CI job

Fix if necessary, and then someone with permission can run bors r+ or bors retry.

Your PR description says "since the latter is mathematically equivalent but stronger according to TC search." but this seems to be a reason not to do the change! In particular,

variable {M : Type*} [CommMonoid M] [Preorder M] [MulLeftMono M] in
#synth IsOrderedMonoid M

is false.

You seem to disagree on what "stronger" means. I am claiming

variable {M : Type*} [CommMonoid M] [Preorder M] [MulLeftMono M] in
#synth IsOrderedMonoid M

fails while

variable {M : Type*} [CommMonoid M] [Preorder M] [IsOrderedMonoid M] in
#synth MulLeftMono M

works.

bors merge

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-CI job
• ci (staging) / Build
• ci (staging) / Test and lint
• ci (staging) / Lint style
• ci (staging) / Post-Build Step

Indeed, and that's why your justification doesn't quite make sense. Note that mathlib doesn't even have a constructor proving the equivalence you mention. Specifically, in an application where my type is unconditionally a Group with MulLeftMono, but only commutative under other conditions, there's no convenient way in mathlib at the moment to build the IsOrderedMonoid instance, and so it's more difficult to apply this theorem after this change :(

Bhavik's suggested constructors were merged in #43663.